Inference at * 2 2 2 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. 0 < ||L1||
7. 0 < ||L2||
8. x = last(L1)
9. y = hd(L2)
  y = (L1 @ L2)[((||L1|| - 1)+1)] 

latex

 by ((RWO "select_append_back" 0) 
CollapseTHEN (Auto')) 

latex

C1: 

C1:   y = L2[(((||L1|| - 1)+1) - ||L1||)]
C.

Definitions	P  Q, x:A. B(x), P  Q, {x:A| B(x)} , i  j < k, P & Q, x:A  B(x), A  B, A, False, P  Q, x:AB(x), Void, {i..j}, , t  T, hd(l), l[i], n+m, n - m, #$n, last(L), a < b, type List, Type, s = t, ||as||, i  j
Lemmas	iff wf, rev implies wf, select append back, le wf